POPL 2018 (series) / CoqPL 2018 (series) /
CoqPL 2018 Program
This is the CoqPL 2018 program - see the full program for POPL 2018 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sat 13 JanDisplayed time zone: Tijuana, Baja California change
Sat 13 Jan
Displayed time zone: Tijuana, Baja California change
09:00 - 10:00 | |||
09:00 60mTalk | CoqHammer: Strong Automation for Program Verification CoqPL File Attached |
10:30 - 12:10 | |||
10:30 25mTalk | A “destruct” Tactic for Mtac2 CoqPL File Attached | ||
10:55 25mTalk | Typed Template Coq CoqPL Simon Boulier , Matthieu Sozeau Inria, Nicolas Tabareau Inria, France, Abhishek Anand Cornell University File Attached | ||
11:20 25mTalk | Elpi: an extension language for Coq CoqPL Enrico Tassi INRIA File Attached | ||
11:45 25mTalk | Coqatoo: Generating Natural Language Versions of Coq Proofs CoqPL Andrew Bedford Laval University File Attached |
14:00 - 14:50 | |||
14:00 25mTalk | Locally Nameless at Scale CoqPL Stephanie Weirich University of Pennsylvania, USA, Antoine Voizard University of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of Pennsylvania File Attached | ||
14:25 25mTalk | A Coq Formalisation of a Core of R CoqPL Martin Bodin CMM File Attached |
14:50 - 15:30 | |||
14:50 40mTalk | Session with the Coq Development Team CoqPL File Attached |
16:00 - 18:05 | |||
16:00 25mTalk | Phantom Types for Quantum Programs CoqPL Robert Rand University of Pennsylvania, Jennifer Paykin University of Pennsylvania, Steve Zdancewic University of Pennsylvania File Attached | ||
16:25 25mTalk | Revisiting Parametricity: Inductives and Uniformity of Propositions CoqPL File Attached | ||
16:50 25mTalk | Towards Context-Aware Data Refinement CoqPL Paul Krogmeier Purdue University, Steven Kidd Purdue University, Benjamin Delaware Purdue University File Attached | ||
17:15 25mTalk | Mechanizing the Construction and Rewriting of Proper Functions in Coq CoqPL Edwin Westbrook Galois, Inc. File Attached | ||
17:40 25mTalk | A calculus for logical refinements in separation logic CoqPL File Attached |